\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$, $T$:Top, ${\it ks}$:Top List, $a$:Top, ${\it snd}$:msg{-}spec(${\it ds}$;${\it da}$),\+
\\[0ex]$j$:Id.
\-\\[0ex]R{-}has{-}loc(ecl{-}machine3(${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;$a$;${\it snd}$);$j$)
\\[0ex]$\sim$
\\[0ex]if \=null(${\it ks}$)$\rightarrow$\+
\\[0ex]reduce($\lambda$$l$,$b$. $\neg_{2}$null(ecl{-}tags($l$;${\it snd}$)) $\wedge_{2}$ source($l$) = $j$
\\[0ex]$\vee_{2}$ $b$;false$_{2}$;remove{-}repeats(IdLnkDeq;msg{-}spec{-}links(${\it snd}$)))
\-\\[0ex]else \=reduce($\lambda$$l$,$b$. source($l$) = $j$\+
\\[0ex]$\vee_{2}$ $b$;false$_{2}$;remove{-}repeats(IdLnkDeq;msg{-}spec{-}links(${\it snd}$))) fi
\-
\end{tabbing}